\section{Conclusion}
\label{sec:conclusion}

\begin{figure}
	\center
	\includegraphics[width=.7\linewidth]{images/iter-modeling.pdf}
	\caption{Generalisation of our approach.}
	\label{fig:iter-modeling}	
%	\vspace{-0.4cm}
\end{figure}


In this paper, we presented a preliminary study on invariant preservation of
behavioral models expressed in Algebraic Petri Nets, in the context of an
iterative modeling process. Given a set of requirements and a metamodel for a
Multi-Level Security File System, we developed a first \textsc{Apn} model. We
also mapped the set of requirements from onto properties expressed as
\textsc{Apn} invariants. For each property that is not satisfied after running a
model checker, we iteratively evolve the model to a next version in order to
eventually satisfy that property while preserving properties that were already
implemented. We also provide a formal mathematical proof of our proposed model
evolution theory based on invariant preservation. Our case study shows the
feasibility of our approach and, to a certain extent, that the evolution
constraints we consider are not too restrictive but in fact usable to solve
engineering problems.

Our future research is concerned with an extension to enhance our theory to
preserve other kinds of properties besides invariants, for example liveness
properties~\cite{DBLP:conf/dfg/PadbergU03}, temporal properties, \emph{etc} by
using existing work in the literature. Furthermore, we would like to support the
integration of modeling language with higher level of abstraction than
\textsc{Apn}, namely Domain-Specific Languages in general. This generalisation
of our approach is illustrated in~\Fig\ref{fig:iter-modeling}.
% Given a set of
% requirements, the modeler develops a domain-specific model (\textsc{Dsm}) as well as a set of
% properties in consistence with the requirements. Then, both the \textsc{Dsm} and
% the set of properties are transformed into models in the \textsc{Apn} formalism
% to perform verification and analysis via the \textsc{Apn} model
% checker~\cite{Lucio2011}. When a new version of the \textsc{Dsm} is produced in
% accordance with specification update, the evolved \textsc{Dsm} and its
% properties are in turn transformed into \textsc{Apn}.

The preservation of the properties at the \textsc{Dsm} level can be achieved by
making use of the commuting diagram in \Fig \ref{fig:iter-modeling}. In order to
verify that an iteration at the \textsc{Dsm} level is property preserving
(formally, $evolve_{DSM}\,\circ\,translate$), we check that it's counterpart at
the \textsc{Apn} level is also property preserving (formally,
$translate\,\circ\,evolve_{APN}$). Of course, in order to do this we have to be
sure that the translations of both the \textsc{Dsl}s models into \textsc{Apn}s
models and properties at the \textsc{Dsl} level into properties at the
\textsc{Apn} level are formally verified. Finally, larger case studies are
necessary to validate the usability of our work in engineering environments.

We think the theory presented in this paper contributes to simplifying
the complexity of model evolution and can be used as a
fundamental ``infrastructure'' for the safe evolution of behavioral models
tackling different domains.

% \smallskip\noindent
% \textbf{Aknowledgements:} This work is partially supported by the Luxemburgish
% Fonds National de la Recherche (\textsc{Fnr}), and contributes to the
% \textsc{Fnr} \textsc{Miter} project. It is also partially funded the the
% Canadian NSERC in the context of the NECSIS project.
